$\forall$${\it es}$:event\_system\{i:l\}. SWellFounded(es{-}pred!(${\it es}$; $e$; ${\it e'}$))